YES 1.655 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((isPrefixOf :: (Eq a, Eq b) => [Either a b ->  [Either a b ->  Bool) :: (Eq a, Eq b) => [Either a b ->  [Either a b ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] _ True
isPrefixOf [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((isPrefixOf :: (Eq b, Eq a) => [Either b a ->  [Either b a ->  Bool) :: (Eq a, Eq b) => [Either b a ->  [Either b a ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (isPrefixOf :: (Eq b, Eq a) => [Either a b ->  [Either a b ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy1100), Succ(xy4001000)) → new_primPlusNat(xy1100, xy4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy300100), Succ(xy400100)) → new_primMulNat(xy300100, Succ(xy400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy30000), Succ(xy40000)) → new_primEqNat(xy30000, xy40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs3(Left(Just(xy3000)), Left(Just(xy4000)), app(ty_Maybe, app(ty_Maybe, bbe)), bbh) → new_esEs2(xy3000, xy4000, bbe)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), bd), app(app(app(ty_@3, dg), dh), ea)), bbh) → new_esEs(xy3002, xy4002, dg, dh, ea)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_[], gg)), gf), bbh) → new_esEs0(xy3000, xy4000, gg)
new_esEs2(Just(xy3000), Just(xy4000), app(app(app(ty_@3, bag), bah), bba)) → new_esEs(xy3000, xy4000, bag, bah, bba)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_Either, cb), cc), bd, be) → new_esEs3(xy3000, xy4000, cb, cc)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, bd, app(ty_[], eb)) → new_esEs0(xy3002, xy4002, eb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_[], gg), gf) → new_esEs0(xy3000, xy4000, gg)
new_esEs3(Right(xy300), Right(xy400), bcc, app(app(ty_Either, bdc), bdd)) → new_esEs3(xy300, xy400, bdc, bdd)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, app(ty_Maybe, dd), be) → new_esEs2(xy3001, xy4001, dd)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, he), app(app(ty_Either, bae), baf)), bbh) → new_esEs3(xy3001, xy4001, bae, baf)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), bd), app(ty_Maybe, ee)), bbh) → new_esEs2(xy3002, xy4002, ee)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), app(app(app(ty_@3, eh), fa), fb)) → new_esEs(xy3000, xy4000, eh, fa, fb)
new_esEs3(Left(Just(xy3000)), Left(Just(xy4000)), app(ty_Maybe, app(app(ty_@2, bbc), bbd)), bbh) → new_esEs1(xy3000, xy4000, bbc, bbd)
new_esEs2(Just(xy3000), Just(xy4000), app(ty_Maybe, bbe)) → new_esEs2(xy3000, xy4000, bbe)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), he, app(ty_[], baa)) → new_esEs0(xy3001, xy4001, baa)
new_esEs3(Left(xy300), Left(xy400), app(app(ty_Either, bca), bcb), bbh) → new_esEs3(xy300, xy400, bca, bcb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_Maybe, hb), gf) → new_esEs2(xy3000, xy4000, hb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), he, app(app(ty_Either, bae), baf)) → new_esEs3(xy3001, xy4001, bae, baf)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), bd), app(ty_[], eb)), bbh) → new_esEs0(xy3002, xy4002, eb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), he, app(app(ty_@2, bab), bac)) → new_esEs1(xy3001, xy4001, bab, bac)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_@2, gh), ha)), gf), bbh) → new_esEs1(xy3000, xy4000, gh, ha)
new_esEs3(Right(xy300), Right(xy400), bcc, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs(xy300, xy400, bcd, bce, bcf)
new_esEs3(Left(Just(xy3000)), Left(Just(xy4000)), app(ty_Maybe, app(app(ty_Either, bbf), bbg)), bbh) → new_esEs3(xy3000, xy4000, bbf, bbg)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), app(ty_[], da)), be), bbh) → new_esEs0(xy3001, xy4001, da)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], app(app(ty_@2, fd), ff)), bbh) → new_esEs1(xy3000, xy4000, fd, ff)
new_esEs3(Right(xy300), Right(xy400), bcc, app(ty_[], bcg)) → new_esEs0(xy300, xy400, bcg)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_@2, fd), ff)) → new_esEs1(xy3000, xy4000, fd, ff)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_Either, cb), cc)), bd), be), bbh) → new_esEs3(xy3000, xy4000, cb, cc)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), app(app(app(ty_@3, ce), cf), cg)), be), bbh) → new_esEs(xy3001, xy4001, ce, cf, cg)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_Maybe, ca)), bd), be), bbh) → new_esEs2(xy3000, xy4000, ca)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_Maybe, fg)) → new_esEs2(xy3000, xy4000, fg)
new_esEs3(Right(xy300), Right(xy400), bcc, app(ty_Maybe, bdb)) → new_esEs2(xy300, xy400, bdb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_Either, hc), hd), gf) → new_esEs3(xy3000, xy4000, hc, hd)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), he, app(ty_Maybe, bad)) → new_esEs2(xy3001, xy4001, bad)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bg), bh), bd, be) → new_esEs1(xy3000, xy4000, bg, bh)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, app(app(ty_Either, de), df), be) → new_esEs3(xy3001, xy4001, de, df)
new_esEs2(Just(xy3000), Just(xy4000), app(app(ty_Either, bbf), bbg)) → new_esEs3(xy3000, xy4000, bbf, bbg)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, he), app(ty_[], baa)), bbh) → new_esEs0(xy3001, xy4001, baa)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, he), app(app(ty_@2, bab), bac)), bbh) → new_esEs1(xy3001, xy4001, bab, bac)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), gb) → new_esEs0(xy3001, xy4001, gb)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, bd, app(app(ty_Either, ef), eg)) → new_esEs3(xy3002, xy4002, ef, eg)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, app(app(app(ty_@3, gc), gd), ge)), gf), bbh) → new_esEs(xy3000, xy4000, gc, gd, ge)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, app(ty_[], da), be) → new_esEs0(xy3001, xy4001, da)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, app(app(ty_@2, db), dc), be) → new_esEs1(xy3001, xy4001, db, dc)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_[], bf)), bd), be), bbh) → new_esEs0(xy3000, xy4000, bf)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_Maybe, ca), bd, be) → new_esEs2(xy3000, xy4000, ca)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, he), app(app(app(ty_@3, hf), hg), hh)), bbh) → new_esEs(xy3001, xy4001, hf, hg, hh)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, bd, app(ty_Maybe, ee)) → new_esEs2(xy3002, xy4002, ee)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_Maybe, hb)), gf), bbh) → new_esEs2(xy3000, xy4000, hb)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], app(app(app(ty_@3, eh), fa), fb)), bbh) → new_esEs(xy3000, xy4000, eh, fa, fb)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], gb), bbh) → new_esEs0(xy3001, xy4001, gb)
new_esEs3(Left(Just(xy3000)), Left(Just(xy4000)), app(ty_Maybe, app(app(app(ty_@3, bag), bah), bba)), bbh) → new_esEs(xy3000, xy4000, bag, bah, bba)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], app(ty_Maybe, fg)), bbh) → new_esEs2(xy3000, xy4000, fg)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, ba), bb), bc), bd, be) → new_esEs(xy3000, xy4000, ba, bb, bc)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_Either, hc), hd)), gf), bbh) → new_esEs3(xy3000, xy4000, hc, hd)
new_esEs3(Left(Just(xy3000)), Left(Just(xy4000)), app(ty_Maybe, app(ty_[], bbb)), bbh) → new_esEs0(xy3000, xy4000, bbb)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, bd, app(app(ty_@2, ec), ed)) → new_esEs1(xy3002, xy4002, ec, ed)
new_esEs2(Just(xy3000), Just(xy4000), app(app(ty_@2, bbc), bbd)) → new_esEs1(xy3000, xy4000, bbc, bbd)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_Either, fh), ga)) → new_esEs3(xy3000, xy4000, fh, ga)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], app(ty_[], fc)), bbh) → new_esEs0(xy3000, xy4000, fc)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), bd), app(app(ty_@2, ec), ed)), bbh) → new_esEs1(xy3002, xy4002, ec, ed)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), app(app(ty_Either, de), df)), be), bbh) → new_esEs3(xy3001, xy4001, de, df)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), bd), app(app(ty_Either, ef), eg)), bbh) → new_esEs3(xy3002, xy4002, ef, eg)
new_esEs3(Left(:(xy3000, xy3001)), Left(:(xy4000, xy4001)), app(ty_[], app(app(ty_Either, fh), ga)), bbh) → new_esEs3(xy3000, xy4000, fh, ga)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), app(app(ty_@2, db), dc)), be), bbh) → new_esEs1(xy3001, xy4001, db, dc)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(app(ty_@3, ba), bb), bc)), bd), be), bbh) → new_esEs(xy3000, xy4000, ba, bb, bc)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, app(app(app(ty_@3, ce), cf), cg), be) → new_esEs(xy3001, xy4001, ce, cf, cg)
new_esEs2(Just(xy3000), Just(xy4000), app(ty_[], bbb)) → new_esEs0(xy3000, xy4000, bbb)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_@2, gh), ha), gf) → new_esEs1(xy3000, xy4000, gh, ha)
new_esEs3(Left(@2(xy3000, xy3001)), Left(@2(xy4000, xy4001)), app(app(ty_@2, he), app(ty_Maybe, bad)), bbh) → new_esEs2(xy3001, xy4001, bad)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_[], bf), bd, be) → new_esEs0(xy3000, xy4000, bf)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_@2, bg), bh)), bd), be), bbh) → new_esEs1(xy3000, xy4000, bg, bh)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), he, app(app(app(ty_@3, hf), hg), hh)) → new_esEs(xy3001, xy4001, hf, hg, hh)
new_esEs0(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_[], fc)) → new_esEs0(xy3000, xy4000, fc)
new_esEs3(Right(xy300), Right(xy400), bcc, app(app(ty_@2, bch), bda)) → new_esEs1(xy300, xy400, bch, bda)
new_esEs3(Left(@3(xy3000, xy3001, xy3002)), Left(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, cd), app(ty_Maybe, dd)), be), bbh) → new_esEs2(xy3001, xy4001, dd)
new_esEs1(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(app(ty_@3, gc), gd), ge), gf) → new_esEs(xy3000, xy4000, gc, gd, ge)
new_esEs(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), cd, bd, app(app(app(ty_@3, dg), dh), ea)) → new_esEs(xy3002, xy4002, dg, dh, ea)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba, bb) → new_isPrefixOf(xy31, xy41, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: